Artifact of the "Formally Verifying Optimizations with Block Simulations" OOPSLA'23 paper

The goal of this artifact is to show that the optimizations presented in our paper are effectively applied, and proved thanks to our translation validation by symbolic execution mechanism. Moreover, we demonstrate that even on large or randomly generated tests, the validation does not produce any false alarm. The artifact also provides a means of reproducing runtime benchmarks (performance in number of cycles), although this requires specific hardware